a:. n:. (-(n)  a & a  n) 

latex

Definitions

ff, tt, if b then t else f fi , T, True, P  Q, P  Q, P  Q, |i|, , t  T, A c B, P & Q, , x:A. B(x), x:A. B(x), Unit, , , , S  T

Lemmas

mul bounds 1a, qmul-qdiv-cancel, assert of lt int, bnot of le int, eqff to assert, assert of le int, eqtt to assert, iff transitivity, qmul comm qrng, qmul over minus qrng, true wf, squash wf, qmul preserves qle, qle-int, qmul-mul, ifthenelse wf, qminus-minus, int inc rationals, bnot wf, lt int wf, assert wf, bool wf, le int wf, qless-int, nat wf, absval wf, rationals wf, int-rational, qmul wf, qle wf, le wf, int nzero properties, q-elim